User blog:Wythagoras/Some function related to Loader's.
I'm reading the book King found, and I think I understand it a bit. So here are some values of the funtion d(n), which I define to be the largest number expressible in n symbols, using the Coq language in the book. Disclaimer: I'm a beginner at this area. You should not use this information unless you've read the whole book and understand it all. Corrections are always welcome. Symbols All these terms count as one symbol each. I shall use n1, n2, n3, ... for the variables, and f1, f2, f3, ... for functions. Further, the following things are in Coq defined: Numbers and functions *The number 0, represented as O '''(or 0? Both are used) *The number 1? Used on page 95, but I'm not sure. *The Successor function, represented as '''S Definitions *The equals sign in a definition, represented as := *With let we can give a value to a variable *With definition 'we start of a definition *'fun 'is to start a definiton of a function *'Z '''and '''nat are the sets of the integers and the set of the positive integers, respectively. *To define the domain of a variable we use the colon :' *We use the arrow -> to give the domain and codomain of a function Logic *Opening and closing brackets '() *The universal quantifier (\(\forall\)), reprensented as forall *The existential quantifier (\(\exists\)), represented as exists *The logical operator OR, represented as \/ *The logical operator AND, represented as /\ *The logical operator NOT, represented as ~''' *The logical operator IF-THEN, represented as '''=> Other symbols *The less or equal sign, represented as <= *The not equal sign, reprensented as <> *ORELSE, represented as || *'''Set '''refers Domains Variables can be defined with or without domain, if the domain is Z. If the domain is the set of the positive integers, we need to say that, as in n1:nat. Functions always need a domain for some reason. Defining iteration Found in the book, section 4.3.3.2, page 95: 18 symbols iterate: forall A:Set, (A->A)->nat->A->A Defining addition, multiplication, exponentation and the Ackermann function All found in the book, section 4.3.3.2, page 95. Addition 30 symbols iterate: forall A:Set, (A->A)->nat->A->A definition f1: nat -> nat -> nat := iterate nat S Multiplication 51 symbols iterate: forall A:Set, (A->A)->nat->A->A definition f1: nat -> nat -> nat := iterate nat S definition f2: (n1 n2: nat) : nat := iterate nat (f1 n1) n2 0. Exponentation 72 symbols iterate: forall A:Set, (A->A)->nat->A->A definition f1: nat -> nat -> nat := iterate nat S definition f2: (n1 n2: nat) : nat := iterate nat (f1 n1) n2 0. definition f3: (n1 n3: nat) : nat := iterate nat (f2 n1) n3 1. Ackermann function 55 symbols iterate: forall A:Set, (A->A)->nat->A->A definition ackermann (n:nat): nat->nat := iterate (nat->nat) (fun (f: nat->nat)(n1:nat) => iterate nat f (S n1)) n S Here, we also iterate over nat->nat, so we are iterating over the iterations of functions. I believe this defines the one argument Ackermann function \(A(n) = 2\uparrow^{n-1}n\) Iterated Ackermann function 76 symbols iterate: forall A:Set, (A->A)->nat->A->A definition f1 (n:nat): nat->nat := iterate (nat->nat) (fun (f: nat->nat)(n1:nat) => iterate nat f (S n1)) n S definition f2 (n1 n2: nat) : nat := iterate nat (f1 n1) n2 0. \(\omega2\) FGH level 92 symbols, not sure whether correct or not. iterate: forall A:Set, (A->A)->nat->A->A definition f1 (n:nat): nat->nat := iterate (nat->nat) (fun (f: nat->nat)(n1:nat) => iterate nat f (S n1)) n S definition f2 (n:nat): nat->nat := iterate (nat->nat) (fun (f: nat->nat)(n1:nat) => iterate nat f (f1 n1)) n S \(\omega^2\) FGH level 93 symbols, not sure whether correct or not. iterate: forall A:Set, (A->A)->nat->A->A definition f1 (n:nat): nat->(nat->nat) := iterate (nat->(nat->nat)) (fun (f: nat->(nat->nat))(n1:nat) => iterate nat->nat (fun (f: nat->nat)(n2:nat) => iterate nat f (S n2)) n1 n S \(\omega^\omega\) FGH level No program yet. It maps the set S to nat->S. (S->(nat->S)) Values Category:Blog posts